\begin{tabbing}
$\forall$\=${\it loc}$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it knd}$:Knd, $T$:Type, $x$:Id,\+
\\[0ex]$f$:((decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)) + (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](\=${\it ds}$; $x$\+
\\[0ex]))).
\-\-\-\-\\[0ex]Reffect(${\it loc}$; ${\it ds}$; ${\it knd}$; $T$; $x$; $f$) $\in$ es\_realizer\{i:l\}
\end{tabbing}